empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
IF(false, x, l) → TAIL(l)
IF(false, x, l) → HEAD(l)
REV(cons(x, l)) → REV2(x, l)
IF(false, x, l) → LAST(head(l), tail(l))
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
LAST(x, l) → EMPTY(l)
LAST(x, l) → IF(empty(l), x, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IF(false, x, l) → TAIL(l)
IF(false, x, l) → HEAD(l)
REV(cons(x, l)) → REV2(x, l)
IF(false, x, l) → LAST(head(l), tail(l))
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
LAST(x, l) → EMPTY(l)
LAST(x, l) → IF(empty(l), x, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(false, x, l) → LAST(head(l), tail(l))
Used ordering: Polynomial interpretation [25,35]:
LAST(x, l) → IF(empty(l), x, l)
The value of delta used in the strict ordering is 1/16.
POL(empty(x1)) = (1/4)x_1
POL(cons(x1, x2)) = 2 + (4)x_2
POL(tail(x1)) = (1/4)x_1
POL(LAST(x1, x2)) = (4)x_2
POL(head(x1)) = 4
POL(true) = 0
POL(false) = 1/4
POL(IF(x1, x2, x3)) = (1/4)x_1 + (3/2)x_3
POL(nil) = 0
empty(nil) → true
empty(cons(x, l)) → false
tail(nil) → nil
tail(cons(x, l)) → l
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
LAST(x, l) → IF(empty(l), x, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
Used ordering: Polynomial interpretation [25,35]:
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
The value of delta used in the strict ordering is 3/16.
POL(REV2(x1, x2)) = (3/4)x_2
POL(cons(x1, x2)) = 1/4 + (2)x_2
POL(rev2(x1, x2)) = x_2
POL(REV(x1)) = (3/4)x_1
POL(nil) = 0
POL(rev(x1)) = x_1
POL(rev1(x1, x2)) = (7/4)x_1 + (5/2)x_2
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))